--------------------------------------------------------------------------------
--
--  Murphi Model of the HyperWall Architecture
--
--------------------------------------------------------------------------------
--
--  version:      1.0
--
--  written by:   Jason Bau
--  date:         November 2011
--  affiliation:  Stanford University (research assistant)
--
--------------------------------------------------------------------------------
--
--  Modeling the Save / Restore
--  Two schemes the before (HV saves registers) and after (stored in memory not
--  accessible to HV)
-- 
--------------------------------------------------------------------------------

--------------------------------------------------------------------------------
-- constants, types and variables
--------------------------------------------------------------------------------


-- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
const
  --first we have the model options.
  FIXED: false;    --before or after fix
  CHECKINVARIANT12: true;  --check invariants 1 and 2?
  
  NumVMs:          2;
  NumCPUs:         2;
  NumHVs:          2;
  NumRuns:         4;    -- number of times the VM runs
  MaxNonce:        2*NumRuns*NumVMs;
  MaxVal:          4*NumRuns*NumVMs;
  HVMemory:        10;   -- number of suspended states each HV remembers 
  CPUMemory:       10;    -- size of the CPU restore queue
  HVVal:           0;
-- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
type
  HyperVisorId:  scalarset (NumHVs);
  CPUId:         scalarset (NumCPUs);
  VMId:          scalarset (NumVMs);
  PrincipId:     union{HyperVisorId,CPUId};
  
  Nonce: 1..MaxNonce;
  ClearVal: 0..MaxVal;
  EncVal: 0..MaxVal;




  SignedHash : record
    NC:       Nonce;       
    VID:      VMId;      
    ClearRegs:ClearVal;          -- all cleartext stored values other than NC: PS_Data, SS_Data, HS_Data, PC, PTR
    EncRegs:  EncVal;            -- encrypted GP registers
  end;

  StoredState : record
    init:     boolean;           -- if init is set, this stored state is used to initialize and does not require any other fields
    NC:       Nonce;             
    ClearRegs:ClearVal;          -- all cleartext stored values other than NC: PS_Data, SS_Data, HS_Data, PC, PTR
    EncRegs:  EncVal;            -- encrypted GP registers
    EncKey:   PrincipId;         -- who encrypted GP regs (only this principal can decrypt)
    SH:       SignedHash;        -- signed hash over the values; cannot
    SHKey:    PrincipId;         -- who signed the hash (only this principal can write)
  end;
 
  CPU : record
    HV: HyperVisorId;            -- Which Hypervisor is running on me?
    runVM: VMId;                     -- running VM
    RestoreST: multiset[CPUMemory] of StoredState;      -- The states CPU were given to restore from
  end;

  VM : record
    suspended:   boolean;            -- suspended or now
    SusState: StoredState;       -- a record of the state before suspending
    timesRun:   0..NumRuns+2;    -- how many times run
    CPU:      CPUId;             -- CPU VM was running on before last suspend
  end;

  HyperVisor : record
    mem: multiset[HVMemory] of StoredState; 
  end;

  GlobalStates : enum {
    INIT1,
    INIT2,
    INIT3,
    RUN
  };
 
  
    

-- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
var                                         -- state variables for
  hype: array[HyperVisorId] of HyperVisor;  --  HyperVisors 
  cpu:  array[CPUId] of CPU; 
  vms:  array[VMId] of VM;
  nextNonce:    Nonce;
  nextClearVal:  ClearVal;
  nextEncVal:    EncVal;
  globalState:  GlobalStates;


---functions-------------

-- Generate a fresh nonce

function freshNonce(): Nonce;
var tmp: Nonce;
begin
  if nextNonce = MaxNonce then
     error "Ran out of nonces!"
  end;
  tmp := nextNonce;
  nextNonce := nextNonce + 1;
  return tmp;
end;

-- Generate a next ClearVal nonce

function getClearVal(): ClearVal;
var tmp: ClearVal;
begin
  if nextClearVal = MaxVal then
     error "Ran out of ClearVals!"
  end;
  tmp := nextClearVal;
  nextClearVal := nextClearVal + 1;
  return tmp;
end;

-- Generate a EncVal

function getEncVal(): EncVal;
var tmp: EncVal;
begin
  if nextEncVal = MaxVal then
     error "Ran out of EncVals!"
  end;
  tmp := nextEncVal;
  nextEncVal := nextEncVal + 1;
  return tmp;
end;


--------------------------------------------------------------------------------
-- rules
--------------------------------------------------------------------------------


--------------------------------------------------------------------------------

-- Behavior of CPU
-- Context switch.  Choose one VM from suspended list to restore, one VM to suspend
ruleset i: CPUId do
  choose j: cpu[i].RestoreST do
    rule 20 "CPU performs context switch"
      globalState = RUN &
      vms[cpu[i].RestoreST[j].SH.VID].timesRun <= NumRuns
    ==>

    var
      inS:  StoredState; 
      st:   StoredState;
      v:    VMId;
      vs:   VMId;
    begin 
      ---- Saving ----------------
      if (!isundefined(cpu[i].runVM)) then       --If a VM is running, then save it.
   
        undefine st;
        vs:= cpu[i].runVM;
        undefine vms[vs].SusState;
        st.init         := false;
        st.NC           := freshNonce();          --build saved state
        st.ClearRegs    := getClearVal();
        st.EncRegs      := getEncVal();
        st.EncKey       := i;                     --CPU encrypts
        st.SH.NC        := st.NC;                 --build hash
        st.SH.VID       := vs;
        st.SH.ClearRegs := st.ClearRegs;
        st.SH.EncRegs   := st.EncRegs;
        st.SHKey        := i;                     --CPU signs

        --Now keep a record of saved state for comparison at restore time
        vms[vs].SusState.NC       		:= st.NC;                 
        vms[vs].SusState.ClearRegs		:= st.ClearRegs;    
        vms[vs].SusState.EncRegs  		:= st.EncRegs;      
        vms[vs].SusState.EncKey   		:= st.EncKey;      
        vms[vs].SusState.SH.NC    		:= st.SH.NC;
        vms[vs].SusState.SH.VID                 := st.SH.VID;
        vms[vs].SusState.SH.ClearRegs    	:= st.SH.ClearRegs;     
        vms[vs].SusState.SH.EncRegs             := st.SH.EncRegs;   
        vms[vs].SusState.SHKey                  := st.SHKey;        

        vms[vs].suspended := true;
        undefine cpu[i].runVM;

        if (!FIXED) then
          if (multisetcount(x:hype[cpu[i].HV].mem,true) < HVMemory) then
           multisetadd (st,hype[cpu[i].HV].mem); -- hand it to the Hypervisor to store/manipulate
          end;
        else                                     -- in the fixed version, the hypervisor cannot read/write
          multisetadd (st,cpu[i].RestoreST);     -- the saved state, so directly hand it to the restoring queue
        end;

      end;

      ----  Restoring ------------
      undefine inS; 
      inS := cpu[i].RestoreST[j];
      v   := inS.SH.VID;
      multisetremove (j,cpu[i].RestoreST);

      if ((inS.init) |                           --if just initializing, do restore w/o validation
          (                                      --otherwise
           (inS.EncKey = i) &			 --validate this CPU can decode
	   (inS.SHKey = i)  &                    --validate this CPU signed SH
           (inS.SH.NC = inS.NC) &                --validate NC against SH
	   (inS.SH.ClearRegs = inS.ClearRegs) &  --validate clearRegs against SH
           (inS.SH.EncRegs = inS.EncRegs)        --validate encRegs against SH
          )
         )
      then -- passed verification, restore v and go on.
        if (vms[v].timesRun <= NumRuns) then 
            vms[v].timesRun := vms[v].timesRun+1;
        end;
        vms[v].suspended := false;
        cpu[i].runVM := v;
        
        --debugging sanity check (comment out during operation)
        --if (vms[v].timesRun = NumRuns) then error "max runs" end;

        -- NOW check invariants 1 and 2
        if ((CHECKINVARIANT12 & !inS.init) &                -- Check invariants if variable set and not initializing
            ((inS.ClearRegs != vms[v].SusState.ClearRegs) | -- INVARIANT 1 -- Trust Evidence integrity before/after resume
             (inS.EncRegs   != vms[v].SusState.EncRegs)))   -- INVARIANT 2 -- GP Reg integrity before/after resume
        then
           error "Suspend / Resume Integrity Violation!"
        end;
      end;
    end;
  end;
end;



---Behavior of Hypervisor
---It basically will send any of its stored states to the appropriate CPU to try to restore
ruleset i: HyperVisorId do
  choose m: hype[i].mem do
    rule 20 "Hypervisor stores VM context (and possibly replays)"
      globalState = RUN  &
      vms[hype[i].mem[m].SH.VID].suspended
    ==>

    var
          outS: StoredState;   -- outgoing state

    begin
          outS := hype[i].mem[m];
          if (multisetcount(x:cpu[outS.EncKey].RestoreST,true)<CPUMemory) then --if there's space in the queue
            -- replace restore record for this VM
            multisetremovepred(x:cpu[outS.EncKey].RestoreST, cpu[outS.EncKey].RestoreST[x].SH.VID = outS.SH.VID); 
  	    multisetadd(outS,cpu[outS.EncKey].RestoreST);	
          end;	  
    end;
  end; 
end;

---Behavior of Hypervisor
---It basically will send any of its stored states to the appropriate CPU to try to restore
ruleset i: HyperVisorId do
  choose m: hype[i].mem do
    rule 20 "Hypervisor saves VM context and writes its own values"
      globalState = RUN  &
      vms[hype[i].mem[m].SH.VID].suspended
    ==>

    var
          outS: StoredState;   -- outgoing state
          c: CPUId;

    begin
          outS := hype[i].mem[m];
          c := outS.EncKey; --record which CPU it's supposed to go to
          outS.ClearRegs    := HVVal;
          outS.EncRegs      := HVVal;
          outS.EncKey       := i;                  --HV encrypts
          outS.SH.ClearRegs := outS.ClearRegs;
          outS.SH.EncRegs   := outS.EncRegs;
          outS.SHKey        := i;                  --HV signs
          if (multisetcount(x:cpu[c].RestoreST,true)<CPUMemory) then --if there's space in the queue
            -- replace restore record for this VM
            multisetremovepred(x:cpu[c].RestoreST, cpu[c].RestoreST[x].SH.VID = outS.SH.VID); 
  	    multisetadd(outS,cpu[c].RestoreST);	
          end;	  
    end;
  end; 
end;





--------------------------------------------------------------------------------
-- startstate
--------------------------------------------------------------------------------

startstate
  globalState := INIT1;
  nextNonce := 1;
  nextClearVal := 1;
  nextEncVal := 1;
  undefine vms;

  for v:VMId do  -- all VMs start suspended
      vms[v].timesRun:=0;
      vms[v].suspended:=true; 
  end;

  -- initialize HyperVisors
  undefine hype;

  -- initialze CPUs
  undefine cpu; 
 

end;

--- 
-- Some further initialization.  
---

-- Assign each CPU to a Hypervisor

ruleset c: CPUId do
 ruleset h: HyperVisorId do
   rule 50 "Assign CPU to Hypervisor"
      globalState = INIT1
   ==>
      cpu[c].HV:=h;
      if (forall p:CPUId do !isundefined(cpu[p].HV) endforall) then
         globalState := INIT2;
      end;
   end;
 end;
end;


-- Assign each VM to a CPU
ruleset c: CPUId do
 ruleset i: VMId do
   rule 50 "Assign VMs to CPU"
      globalState = INIT2 &
      isundefined(vms[i].CPU) 
   ==>
   var 
      tmp: StoredState;
   begin
      tmp.init:=true;  -- add this VM to the CPU's queue of VMs waiting to be restored
      tmp.SH.VID:=i;
      multisetadd(tmp,cpu[c].RestoreST);
      vms[i].CPU := c;
      if ( forall vm:VMId do 
            !isundefined(vms[vm].CPU) 
           endforall ) 
      then
         globalState := RUN;
	 --error "assigned VMs to CPUs"	
      end;
   end;
 end;
end;




invariant "hypervisor never learns GPRegs" -- invariant 3
forall h:HyperVisorId do
  multisetcount(i:hype[h].mem, hype[h].mem[i].EncKey = h) = 0
end;


